Nuprl Lemma : inl_eq_btrue
4,23
postcript
pdf
x
:Top. inl(
x
) = true
Decision
latex
Definitions
Decision
,
true
,
x
:
A
.
B
(
x
)
,
t
T
,
Top
Lemmas
top
wf
origin
x:Top. inl(x) = true
Decision x:Top. inl(x) = true Decision x:A. B(x) T